(*
  logic simplification.
*)

Section LogicSimplification.

Variables A B C : Prop.

Lemma demorgan_or : ~A /\ ~B -> ~(A \/ B).
Proof.
  tauto.
Qed.

Lemma demorgan_and : ~A \/ ~B -> ~(A /\ B).
Proof.
  tauto.
Qed.

Lemma not_imply : ~(~A \/ B) -> ~(A -> B).
Proof.
  tauto.
Qed.

Lemma not_not : A -> ~~A.
Proof.
  tauto.
Qed.

Lemma not_true : False -> ~True.
Proof.
  tauto.
Qed.

Lemma not_false : True -> ~False.
Proof.
  tauto.
Qed.

End LogicSimplification.

(* simplification by repeated application of above lemmas. *)
Ltac Logic_simplify :=
  match goal with
    | |- context [~(?x1 \/ ?x2)] => apply demorgan_or; Logic_simplify
    | |- ~(?x1 /\ ?x2) => apply demorgan_and; Logic_simplify
    | |- ~(?x1 -> ?x2) => apply not_imply; Logic_simplify
    | |- ~True => apply not_true
    | |- ~False => apply not_false
    | |- ~~?x => apply not_not
    | _ => idtac
end.

(* convert hyp : A<=B |- G to A<B |- G and A=B |- G. *)
Ltac Split_less_than hyp :=
  match type of hyp with
    | ?a <= ?b  =>
      let h1 := fresh "H" in
	assert(h1 : a < b \/ a = b); 
	  [omega|idtac]; elim h1; intro
    | ?c -> ?a <= ?b  =>
      let h1 := fresh "H" in
	assert(h1 : c -> a < b \/ a = b);[omega|idtac];
	  elim h1; try(intro)
    | _ => idtac
  end.
